M1, M2:MsgA.
M1  M2
 (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id,
 (ms:((tg:Id  if source(l) = i then M2.da(rcv(l,tg)) else Top fi ) List).
 M2.send(k;l;s;v;ms;i)  M1.send(k;l;s;v;ms;i)) 

latex

Definitions

x:A. B(x), P  Q, M.da(a), if b then t else f fi , M.send(k;l;s;v;ms;i), t.1, t.2, z != f(x)  P(a;z), t  T, tt, , ff, SQType(T), {T}, x. t(x), S  T, Top, MsgA, M1  M2, M.state, , Valtype(da;k), A c B, P & Q, Unit, P  Q, P  Q, x(s), A, False, f  g,

Lemmas

eq id wf, lsrc wf, bool wf, iff transitivity, assert wf, Id wf, eqtt to assert, assert-eq-id, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, ifthenelse wf, ma-da wf, rcv wf, top wf, ma-st wf, IdLnk wf, Knd wf, ma-sub wf, msga wf, bool cases, bool sq, fpf-dom wf, product-deq wf, Kind-deq wf, idlnk-deq wf, fpf-trivial-subtype-top, ma-state wf, fpf-cap wf, pi1 wf, pi2 wf, concat wf, map wf, fpf-ap wf, fpf-cap-void-subtype, subtype-fpf-cap-top